T:Type, L:(T List). (0 < ||L||)  no_repeats(T;L)  (x:T. x before hd(L)  L  False) 

latex

ProofTree

Definitions	no_repeats(T;l), x before y  l, x:AB(x), P  Q, P  Q, x:A  B(x), P & Q, P  Q, x:A. B(x), False, ||as||, Void, Type, type List, a < b, (x  l), A, x:A. B(x), hd(l), L1  L2, s = t, i  j , #$n, , t  T
Lemmas	l before transitivity, hd-before, l member wf, l before member2, no repeats wf, l before wf, false wf, no repeats iff